A.

(insert publication list)

COMMENTS ON MANNA'S MOST IMPORTANT PUBLICATIONS

by John McCarthy, Professor of Computer Science

1. %2Mathematical Theory of Computation%1, McGraw-Hill, New York 1974.

	This book, which has already been translated into Japanese,
Italian and Russian and reprinted as a paperback, is the first textbook
in mathematical theory of computation.
Its appearance is a major step towards replacing experimental debugging
of computer programs by proofs that they meet their specifications.

	At present, computer programs are debugged.  That is, after
a program is written it is tried on test cases until its author is
satisfied and turns it over to users.  If the program is at all
complex, the users usually find further mistakes.  Mistakes turn
up in big systems for years.  The mistakes often cause economic loss
and the cost of fixing them often exceeds the cost of the original
program many times over.

	The major applied goal of mathematical theory of computation
is to replace debugging by mathematically proving that the program
meets its specifications.  Such a proof must then be checked either
by a person or by a proof-checking computer program.  Once this has
been done, the chance of error is reduced to that of an incongruity
between the formal specifications and what the users have in mind
or to an error in the proof-checking program or on the part of the
human checking the proof.  Computer scientists believe that
formal proving will bring about a major reduction in the cost
of getting good programs.

	Manna's text is the first big step in making these techniques
accessible to students of computer science at an early stage.  Writing
the first textbook in a new field is a major creative endeavor, and
Manna's book is not a mere summary of research papers.  The high regard
the computer science world has for the book is shown by the number
of translations into foreign languages.

	It is a first class scholarly work in that it reworks and presents not
only the approaches to program proving that Manna himself has worked on,
but also the other major approaches and necessary background material
from mathematical logic, recursive function theory and the theory of
automata.

2. "Properties of programs and the first-order predicate calculus",
%2Journal of the Association for Computing Machinery%1, Vol. 16,
No. 2, pp. 244-255. April 1969.

	This paper, based on Manna's Ph.D. thesis, shows how to
write sentences of the predicate calculus expressing the %2total
correctness%1 of a program.  It is a kind of dual to the method
of inductive assertions invented by Robert Floyd which gives only
partial correctness, i.e. that the program give correct results
under the assumption that it terminates.  Manna's new method is
a creative achievement and elegantly presented, but  the Manna
sentences have been difficult to prove.  The method is ripe for
re-examination now that the techniques for proving such sentences
are better developed.

3. - with S. Ness and J. Vuillemin, "Inductive methods for proving
properties of programs", %2Communications of the ACM%1, vol. 16,
No. 8, ppl 491-502. (1973).

	This paper which won an ACM award as the best paper of 1974,
presents a number of methods for proving properties of both recursive
and sequential programs.  One of the methods has been revived by
Morris and Wegbreit under the name of %2subgoal induction%1.
This method is for recursive programs what Floyd's inductive assertion
method is for sequential programs.

4. - 
!B. not applicable
!C. Manna's current research is in three areas - mathematical theory of
computation, computer program synthesis, and other topics in theoretical
computer science.

	Manna has been one of the leaders in mathematical theory of
computation since his thesis in 1968.  He continues to develop new
techniques for proving that computer programs meet their specifications.
Thus, in collaboration with his student Nachum Dershowitz, he has
just completed a paper showing how production system computations
can be proved to terminate by induction on generalized lexicographic
orderings.  This has settled several previously recalcitrant cases.

[good words about program synthesis]
!IV. THE CANDIDATE'S ROLE

A. Description of candidate's expected role.

	Manna will strengthen the Computer Science Department in mathematical
theory of computation and possibly in artificial intelligence.  (His
program synthesis work is going in that direction).  When he was at
Stanford before he directed theses in this area and his careful
work with students has been missed.
He will teach the main courses and take part in curriculum design in these
areas.

	We also expect him to do his share of committee work, and we
consider him capable of taking his turn as department chairman.

B. He has already done all these things extremely successfully.

C. The department as a whole has connections with other departments, but
Manna's field is not especially involved in such collaborations.

D. When Manna was an assistant professor here at Stanford he took part
in the following committee activities.
!V. EVALUATION OF TEACHING

	Manna is an excellent lecturer and is always extremely well
prepared.  Enclosed is a copy of the student course evaluation of his most
recent course taught at Stanford.  It is a research oriented course
in a field in which many of the students were unprepared.
!VI. SEARCH REPORT

	The Computer Science Department has been trying to get an
outstanding researcher and teacher in this field for many years.
In our letters concerning Manna we asked for comparison with the
outstanding people, including Anthony Hoare and Dana Scott of
Oxford, Edsger Dijkstra, and Rod Burstall of Edinburgh.

	Scott was previously at Stanford in the Mathematics Department
and left for Princeton and finally Oxford.  His field overlaps Manna's
slightly, but his strengths are different.
We don't know why he left Stanford, but there is no reason to suppose
he wants to return.
Whether the Department would prefer him if were available has not been
explored.

	Hoare visited Stanford in 1973-74 and his interest in coming
to Stanford was explored with negative result.  Whether we would now
prefer him is unexplored.

	Dijkstra declined a Stanford offer about five years ago.  The
Department would definitely not make him an offer today, because of
a conviction that he is not keeping up with what others have accomplished
in this field.

	Burstall's interest in coming to Stanford was explored several
years ago with negative results.  Whether we would prefer him, were
he available, has not been explored, but the probable answer is negative.

	If either Scott or Hoare were available, we would probably
consider them targets of opportunity.

	In our letters, we asked for recommendations of competitive
candidates and received none.

	We are confident that we know everyone who has made major
contributions to mathematical theory of computation.

	None of the outstanding people in this field are candidates
for affirmative action.
!B. We are considering the appointment of Manna as a new appointment although
he has been here before.  However, because he has been here before,  the
senior faculty know Manna's work very well and unanimously support the
appointment.
!VII. DEPARTMENT APPROVAL
A.

B. The Department Appointments and Promotions Committee conducted tee
search and unanimously recommended appointment to a tenured position.
The Department tenured faculty unanimously repeated this recommendation,
and the Department Professors unanimously recommended the rank of
Professor.

C. All members voted.

D. Approval was unanimous.